\section{Reproducibility}
In order to let the user reproduce our results we advice to take the following steps.
\begin{itemize}
\item We advice to use: 32 bits Java $\geq$ version 5 Second Edition.
\item JavaBDD is included in the source and needs not to be set as environment variable or in the classpath.
\item If you do not use 32 bits Java, BuDDy will not be used, but a slower Java implementation will be used.
\item In the root folder of our model checker there two bash scripts. One for compiling \emph{compile} and one for running \emph{run}. We tested our build scripts for only linux, but it should work on Mac.
\end{itemize}
How to use the model checker:
\begin{enumerate}
\item Go to the root folder of our model checker.
\item Compile the code: \emph{\$ ./compile}
%\item Run the code: \emph{\$ ./run screens/screen.n} where n is a screen number.
\item Open the bin folder \emph{\$ cd bin}
\item Run the code: \emph{\$ .java -Xms3500m -Xmx3501m soko.Sokoban ../screens/screen.n} where n is a screen number.
\item An alternative way to run the program (without needing to compile) is to use Sokoban.jar. Run this with the command \emph{java -cp Sokoban.jar soko.Sokoban} with the path to a screen file as an argument.
\item Optionally you can one of the following switches:
\begin{itemize}
\item \emph{-d}: enable to look for the (shortest) trace to an unsolvable state.
\item \emph{-nodeadlockremoval}: do not remove deadlock states (results in slower computations with more states).
\item \emph{-countsolutions}: count the number of reachable solution states.
\item \emph{-lurd lurdstring}: apply the lurdstring (consisting of l u r and d characters) to the initial state before solving.
\end{itemize}
\end{enumerate}
